.po 0
.nr PO 0.5i
.nr LL 7.0i
.ND
.TL
Assistance in Hierarchical and Structured Logic Design 
Using Temporal Logic and Prolog
.AU
 Masahiro FUJITA *
 Shinji KONO 
 Hidehiko TANAKA 
 Tohru MOTO-OKA 
.AI
 Department of Electrical Engineering
 University of Tokyo
 Hongo Bunkyo_ku
 Tokyo, Japan
 *: Now at Fujitsu Laboratories Ltd.
    Kawasaki, Japan
.ls 2
.AB
We have been studying on assistance to hardware logic design,
using Temporal Logic, called Linear Time Temporal Logic
(LTTL)[6],  and Prolog [13].
Generally speaking, a hardware system can be divided into two parts: 
functional part, which performs logical and arithmetic operations, and
a synchronization part, 
which controls timing for data transfers among function units.
Efficient verification and synthesis techniques for synchronization
have been proposed in [11,12,13].
In this paper, we first review our specification techniques for synchronization
parts using LTTL.
Then we present a Temporal logic programming language based on LTTL
called Tokio which includes interval variables.
Though parallelisms are easily expressed in LTTL, it is tedious to describe
sequentiality in LTTL.
So here we introduce the notion of interval variables,
which express a finite number of successive times, to LTTL.
The efficient verification and synthesis techniques of LTTL can be applied
to Tokio programs for synchronization parts since interval variables are
derived from a combination of LTTL and Tokio.
The resulting LTTL with interval variables is
a subset of Interval Temporal Logic
(ITL) developed by Moszkowski [7,8,9].
He also developed Tempura,
a programming language based upon ITL.
Tokio not only incorporates various Tempura operators,
but also it is a resolution base logic programming language
that includes backtracking and unification.
Using these tools and techniques, hierarchical and structured design
can be smoothly supported.
.AE
.NH
Introduction
.PP
Digital systems have grown too large to design without computer
assistance.
The many efforts in the direction fo hardware design assistance have
focussed primarily an the implementation of an existing design.
We here discuss assistance of logic design, where inputs are specifications
and outputs are networks of logical gates or equivalent level design.
.PP
Hierarchical and structured designs are considered to be the most
effective approach for large and complex systems.
Hierarchical and structured design is the repetition of the following
until all the sub-modules can easily be implemented with physical components:
.IP (1)
specifying the hardware module to be designed
.IP (2)
separating it into several sub-modules and designing them and verifying
that the designs for the decomposed sub-modules really satisfy 
the specification,
.LP
or
.IP (2)
automatically synthesizing designs from the specification.
.PP
Therefore, it is important to devise techniques of the 
following areas:
.IP (1)
specification
.IP (2)
formal verification
.IP (3)
automatic synthesis
.LP
Moreover, formal verification is difficult especially in the
case of large systems.
In earlier stages of designs, designers  used to assure their designs by
simulations.
Thus a simple simulation facility is
as important as formal verification:
.IP (4)
simulation.
.PP
Formal verification and automatic synthesis
require formal specification techniques that are
mathematically sound.
There have been a number of specification techniques including HDLs [1],
but they are mainly intend for simulations
and lack the necessary mathematical rigor.
Elegant hardware specification require formal methods capability
of expressing parallelism to reflect the essentially parallel
operation of th hardware itself.
CCS [2] and Temporal Logic [3] are examples of such models.
Some researchers have begun to apply them to hardware verification and
synthesis [4,5].
.PP
In this paper, we use 
Linear Time Temporal Logic (LTTL) [6] as a hardware specification language.
We have already developed efficient verification and synthesis techniques for
propositional LTTL [11,12,13].
Propositional LTTL has a decision procedure and is assisted efficiently.
However, there is a disadvantage:
although parallelisms are easily described in LTTL, some properties,
such as sequentiality, are not so easy to describe.
.PP
Moszkowski proposed Interval Temporal Logic (ITL) [7] and a programming
language called Tempura [8] that is based upon ITL.
Sequentiality as well as parallelism is easily described in ITL.
Recently, he developed an interpreter for a subset of Tempura in Lisp [9],
which can directly execute specification in Tempura.
.PP
However, mechanical reasoning is not yet done for ITL.
In this purpose, 
we introduce the ITL notion of interval to LTTL, which makes it 
easy to describe sequentiality as well as parallelism in LTTL, while
ease of mechanical reasonings remains.
We also present a logic programming language, whose name is Tokio, 
which is very similar to Tempura
but based upon first order LTTL and Prolog [10], and its interpreter.
The language has a syntax similar to Prolog and is a natural extension of
Prolog to handle temporal reasonings.
.PP
Moreover, the technique for separating a Tokio program into a function part,
which executes logical and arithmetic functions and is expressed in
first order logic, and a  synchronization part,
which controls timing for data transfer among function units and
is expressed in propositional logic, exists.
So we can apply efficient verification and synthesis technique [11,12,13]
to synchronization parts, even when designs are described in Tokio, i.e, 
first order LTTL.
.PP
In this paper,
we first present specification techniques for
synchronization parts in propositional LTTL.
We then introduce a  programming language Tokio and its interpreter,
which can emulate both synchronization and functional parts.
